\begin{tabbing}
$\forall$\=$T$:Type, $L$:($T$ List), $P$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow\mathbb{B}$), ${\it T'}$:Type,\+
\\[0ex]$f$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) c$\wedge$ ($\uparrow$($P$($x$)))\} $\rightarrow$${\it T'}$), $x$:${\it T'}$.
\-\\[0ex]($x$ $\in$ mapfilter($f$;$P$;$L$)) $\Leftarrow\!\Rightarrow$ ($\exists$$y$:$T$. (($y$ $\in$ $L$) \& (($\uparrow$($P$($y$))) c$\wedge$ ($x$ = $f$($y$)))))
\end{tabbing}